Nuprl Lemma : compose-fpf_wf 11,40
A:Type, B:(AType), f:fpf(A; x.B(x)), C:Type, a:(A(?C)), b:(CA).
(y:A. (isl(a(y)))  (b(outl(a(y))) = y))  (compose-fpf(a; b; f)  fpf(C; y.B(b(y)))) 
latex

Definitionst  T, x:A. B(x), (x  l), A c B, Unit, isl(x), P  Q, x:A. B(x), b, True, T, P  Q, SqStable(P), , outl(x), P  Q, mapfilter(f; P; L), compose(f; g), fpf-domain(f), fpf(A; a.B(a)), t.2, x(s), compose-fpf(a; b; f), x. t(x), prop{i:l}
Lemmassquash wf, true wf, fpf wf, mapfilter wf, member map filter, outl wf, sq stable from decidable, decidable assert, assert wf, isl wf, unit wf, l member wf

origin